(set-option :TIMEOUT 120000)
(declare-const N1 Int)
(assert (and (>= N1 0) (<= N1 1)))
(declare-const C1_0 Int)
(assert (and (>= C1_0 0) (<= C1_0 1)))
(declare-const C1_1 Int)
(assert (and (>= C1_1 0) (<= C1_1 1)))
(declare-const C1_2 Int)
(assert (and (>= C1_2 0) (<= C1_2 1)))
(declare-const C1_3 Int)
(assert (and (>= C1_3 0) (<= C1_3 1)))
(declare-const C1_4 Int)
(assert (and (>= C1_4 0) (<= C1_4 1)))
(declare-const C1_5 Int)
(assert (and (>= C1_5 0) (<= C1_5 1)))
(declare-const C1_6 Int)
(assert (and (>= C1_6 0) (<= C1_6 1)))
(declare-const C1_7 Int)
(assert (and (>= C1_7 0) (<= C1_7 1)))
(declare-const C1_8 Int)
(assert (and (>= C1_8 0) (<= C1_8 1)))
(declare-const C1_9 Int)
(assert (= C1_9 0))
(declare-const C1_10 Int)
(assert (and (>= C1_10 0) (<= C1_10 1)))
(declare-const C1_11 Int)
(assert (and (>= C1_11 0) (<= C1_11 1)))
(declare-const C1_12 Int)
(assert (and (>= C1_12 0) (<= C1_12 1)))
(declare-const C1_13 Int)
(assert (and (>= C1_13 0) (<= C1_13 1)))
(declare-const C1_14 Int)
(assert (and (>= C1_14 0) (<= C1_14 1)))
(declare-const C1_15 Int)
(assert (and (>= C1_15 0) (<= C1_15 1)))
(declare-const N2 Int)
(assert (and (>= N2 0) (<= N2 1)))
(declare-const C2_0 Int)
(assert (and (>= C2_0 0) (<= C2_0 1)))
(declare-const C2_1 Int)
(assert (and (>= C2_1 0) (<= C2_1 1)))
(declare-const C2_2 Int)
(assert (and (>= C2_2 0) (<= C2_2 1)))
(declare-const C2_3 Int)
(assert (and (>= C2_3 0) (<= C2_3 1)))
(declare-const C2_4 Int)
(assert (= C2_4 0))
(declare-const C2_5 Int)
(assert (and (>= C2_5 0) (<= C2_5 1)))
(declare-const C2_6 Int)
(assert (and (>= C2_6 0) (<= C2_6 1)))
(declare-const C2_7 Int)
(assert (and (>= C2_7 0) (<= C2_7 1)))
(declare-const C2_8 Int)
(assert (and (>= C2_8 0) (<= C2_8 1)))
(declare-const C2_9 Int)
(assert (and (>= C2_9 0) (<= C2_9 1)))
(declare-const C2_10 Int)
(assert (and (>= C2_10 0) (<= C2_10 1)))
(declare-const C2_11 Int)
(assert (and (>= C2_11 0) (<= C2_11 1)))
(declare-const C2_12 Int)
(assert (and (>= C2_12 0) (<= C2_12 1)))
(declare-const C2_13 Int)
(assert (and (>= C2_13 0) (<= C2_13 1)))
(declare-const C2_14 Int)
(assert (and (>= C2_14 0) (<= C2_14 1)))
(declare-const C2_15 Int)
(assert (and (>= C2_15 0) (<= C2_15 1)))
(declare-const N10 Int)
(assert (and (>= N10 0) (<= N10 1)))
(declare-const C10_0 Int)
(assert (and (>= C10_0 0) (<= C10_0 1)))
(declare-const C10_1 Int)
(assert (and (>= C10_1 0) (<= C10_1 1)))
(declare-const C10_2 Int)
(assert (and (>= C10_2 0) (<= C10_2 1)))
(declare-const C10_3 Int)
(assert (and (>= C10_3 0) (<= C10_3 1)))
(declare-const C10_4 Int)
(assert (and (>= C10_4 0) (<= C10_4 1)))
(declare-const C10_5 Int)
(assert (and (>= C10_5 0) (<= C10_5 1)))
(declare-const C10_6 Int)
(assert (and (>= C10_6 0) (<= C10_6 1)))
(declare-const C10_7 Int)
(assert (and (>= C10_7 0) (<= C10_7 1)))
(declare-const C10_8 Int)
(assert (and (>= C10_8 0) (<= C10_8 1)))
(declare-const C10_9 Int)
(assert (and (>= C10_9 0) (<= C10_9 1)))
(declare-const C10_10 Int)
(assert (and (>= C10_10 0) (<= C10_10 1)))
(declare-const C10_11 Int)
(assert (and (>= C10_11 0) (<= C10_11 1)))
(declare-const C10_12 Int)
(assert (and (>= C10_12 0) (<= C10_12 1)))
(declare-const C10_13 Int)
(assert (and (>= C10_13 0) (<= C10_13 1)))
(declare-const C10_14 Int)
(assert (and (>= C10_14 0) (<= C10_14 1)))
(declare-const C10_15 Int)
(assert (= C10_15 0))
(declare-const N11 Int)
(assert (and (>= N11 0) (<= N11 1)))
(declare-const C11_0 Int)
(assert (and (>= C11_0 0) (<= C11_0 1)))
(declare-const C11_1 Int)
(assert (and (>= C11_1 0) (<= C11_1 1)))
(declare-const C11_2 Int)
(assert (and (>= C11_2 0) (<= C11_2 1)))
(declare-const C11_3 Int)
(assert (= C11_3 0))
(declare-const C11_4 Int)
(assert (and (>= C11_4 0) (<= C11_4 1)))
(declare-const C11_5 Int)
(assert (and (>= C11_5 0) (<= C11_5 1)))
(declare-const C11_6 Int)
(assert (and (>= C11_6 0) (<= C11_6 1)))
(declare-const C11_7 Int)
(assert (and (>= C11_7 0) (<= C11_7 1)))
(declare-const C11_8 Int)
(assert (and (>= C11_8 0) (<= C11_8 1)))
(declare-const C11_9 Int)
(assert (and (>= C11_9 0) (<= C11_9 1)))
(declare-const C11_10 Int)
(assert (and (>= C11_10 0) (<= C11_10 1)))
(declare-const C11_11 Int)
(assert (and (>= C11_11 0) (<= C11_11 1)))
(declare-const C11_12 Int)
(assert (and (>= C11_12 0) (<= C11_12 1)))
(declare-const C11_13 Int)
(assert (and (>= C11_13 0) (<= C11_13 1)))
(declare-const C11_14 Int)
(assert (and (>= C11_14 0) (<= C11_14 1)))
(declare-const C11_15 Int)
(assert (and (>= C11_15 0) (<= C11_15 1)))
(declare-const N12 Int)
(assert (and (>= N12 0) (<= N12 1)))
(declare-const C12_0 Int)
(assert (and (>= C12_0 0) (<= C12_0 1)))
(declare-const C12_1 Int)
(assert (and (>= C12_1 0) (<= C12_1 1)))
(declare-const C12_2 Int)
(assert (and (>= C12_2 0) (<= C12_2 1)))
(declare-const C12_3 Int)
(assert (and (>= C12_3 0) (<= C12_3 1)))
(declare-const C12_4 Int)
(assert (= C12_4 0))
(declare-const C12_5 Int)
(assert (and (>= C12_5 0) (<= C12_5 1)))
(declare-const C12_6 Int)
(assert (and (>= C12_6 0) (<= C12_6 1)))
(declare-const C12_7 Int)
(assert (and (>= C12_7 0) (<= C12_7 1)))
(declare-const C12_8 Int)
(assert (and (>= C12_8 0) (<= C12_8 1)))
(declare-const C12_9 Int)
(assert (and (>= C12_9 0) (<= C12_9 1)))
(declare-const C12_10 Int)
(assert (and (>= C12_10 0) (<= C12_10 1)))
(declare-const C12_11 Int)
(assert (and (>= C12_11 0) (<= C12_11 1)))
(declare-const C12_12 Int)
(assert (and (>= C12_12 0) (<= C12_12 1)))
(declare-const C12_13 Int)
(assert (and (>= C12_13 0) (<= C12_13 1)))
(declare-const C12_14 Int)
(assert (and (>= C12_14 0) (<= C12_14 1)))
(declare-const C12_15 Int)
(assert (and (>= C12_15 0) (<= C12_15 1)))
(declare-const N13 Int)
(assert (and (>= N13 0) (<= N13 1)))
(declare-const C13_0 Int)
(assert (and (>= C13_0 0) (<= C13_0 1)))
(declare-const C13_1 Int)
(assert (and (>= C13_1 0) (<= C13_1 1)))
(declare-const C13_2 Int)
(assert (and (>= C13_2 0) (<= C13_2 1)))
(declare-const C13_3 Int)
(assert (and (>= C13_3 0) (<= C13_3 1)))
(declare-const C13_4 Int)
(assert (and (>= C13_4 0) (<= C13_4 1)))
(declare-const C13_5 Int)
(assert (and (>= C13_5 0) (<= C13_5 1)))
(declare-const C13_6 Int)
(assert (and (>= C13_6 0) (<= C13_6 1)))
(declare-const C13_7 Int)
(assert (and (>= C13_7 0) (<= C13_7 1)))
(declare-const C13_8 Int)
(assert (and (>= C13_8 0) (<= C13_8 1)))
(declare-const C13_9 Int)
(assert (and (>= C13_9 0) (<= C13_9 1)))
(declare-const C13_10 Int)
(assert (and (>= C13_10 0) (<= C13_10 1)))
(declare-const C13_11 Int)
(assert (and (>= C13_11 0) (<= C13_11 1)))
(declare-const C13_12 Int)
(assert (and (>= C13_12 0) (<= C13_12 1)))
(declare-const C13_13 Int)
(assert (and (>= C13_13 0) (<= C13_13 1)))
(declare-const C13_14 Int)
(assert (and (>= C13_14 0) (<= C13_14 1)))
(declare-const C13_15 Int)
(assert (and (>= C13_15 0) (<= C13_15 1)))
(declare-const N17 Int)
(assert (and (>= N17 0) (<= N17 1)))
(declare-const C17_0 Int)
(assert (and (>= C17_0 0) (<= C17_0 1)))
(declare-const C17_1 Int)
(assert (and (>= C17_1 0) (<= C17_1 1)))
(declare-const C17_2 Int)
(assert (and (>= C17_2 0) (<= C17_2 1)))
(declare-const C17_3 Int)
(assert (and (>= C17_3 0) (<= C17_3 1)))
(declare-const C17_4 Int)
(assert (and (>= C17_4 0) (<= C17_4 1)))
(declare-const C17_5 Int)
(assert (and (>= C17_5 0) (<= C17_5 1)))
(declare-const C17_6 Int)
(assert (and (>= C17_6 0) (<= C17_6 1)))
(declare-const C17_7 Int)
(assert (and (>= C17_7 0) (<= C17_7 1)))
(declare-const C17_8 Int)
(assert (and (>= C17_8 0) (<= C17_8 1)))
(declare-const C17_9 Int)
(assert (and (>= C17_9 0) (<= C17_9 1)))
(declare-const C17_10 Int)
(assert (and (>= C17_10 0) (<= C17_10 1)))
(declare-const C17_11 Int)
(assert (and (>= C17_11 0) (<= C17_11 1)))
(declare-const C17_12 Int)
(assert (and (>= C17_12 0) (<= C17_12 1)))
(declare-const C17_13 Int)
(assert (and (>= C17_13 0) (<= C17_13 1)))
(declare-const C17_14 Int)
(assert (and (>= C17_14 0) (<= C17_14 1)))
(declare-const C17_15 Int)
(assert (= C17_15 0))
(declare-const N18 Int)
(assert (and (>= N18 0) (<= N18 1)))
(declare-const C18_0 Int)
(assert (and (>= C18_0 0) (<= C18_0 1)))
(declare-const C18_1 Int)
(assert (and (>= C18_1 0) (<= C18_1 1)))
(declare-const C18_2 Int)
(assert (and (>= C18_2 0) (<= C18_2 1)))
(declare-const C18_3 Int)
(assert (and (>= C18_3 0) (<= C18_3 1)))
(declare-const C18_4 Int)
(assert (and (>= C18_4 0) (<= C18_4 1)))
(declare-const C18_5 Int)
(assert (and (>= C18_5 0) (<= C18_5 1)))
(declare-const C18_6 Int)
(assert (and (>= C18_6 0) (<= C18_6 1)))
(declare-const C18_7 Int)
(assert (and (>= C18_7 0) (<= C18_7 1)))
(declare-const C18_8 Int)
(assert (and (>= C18_8 0) (<= C18_8 1)))
(declare-const C18_9 Int)
(assert (and (>= C18_9 0) (<= C18_9 1)))
(declare-const C18_10 Int)
(assert (and (>= C18_10 0) (<= C18_10 1)))
(declare-const C18_11 Int)
(assert (and (>= C18_11 0) (<= C18_11 1)))
(declare-const C18_12 Int)
(assert (and (>= C18_12 0) (<= C18_12 1)))
(declare-const C18_13 Int)
(assert (and (>= C18_13 0) (<= C18_13 1)))
(declare-const C18_14 Int)
(assert (and (>= C18_14 0) (<= C18_14 1)))
(declare-const C18_15 Int)
(assert (and (>= C18_15 0) (<= C18_15 1)))
(declare-const N19 Int)
(assert (and (>= N19 0) (<= N19 1)))
(declare-const C19_0 Int)
(assert (and (>= C19_0 0) (<= C19_0 1)))
(declare-const C19_1 Int)
(assert (and (>= C19_1 0) (<= C19_1 1)))
(declare-const C19_2 Int)
(assert (and (>= C19_2 0) (<= C19_2 1)))
(declare-const C19_3 Int)
(assert (and (>= C19_3 0) (<= C19_3 1)))
(declare-const C19_4 Int)
(assert (and (>= C19_4 0) (<= C19_4 1)))
(declare-const C19_5 Int)
(assert (and (>= C19_5 0) (<= C19_5 1)))
(declare-const C19_6 Int)
(assert (and (>= C19_6 0) (<= C19_6 1)))
(declare-const C19_7 Int)
(assert (and (>= C19_7 0) (<= C19_7 1)))
(declare-const C19_8 Int)
(assert (and (>= C19_8 0) (<= C19_8 1)))
(declare-const C19_9 Int)
(assert (and (>= C19_9 0) (<= C19_9 1)))
(declare-const C19_10 Int)
(assert (and (>= C19_10 0) (<= C19_10 1)))
(declare-const C19_11 Int)
(assert (and (>= C19_11 0) (<= C19_11 1)))
(declare-const C19_12 Int)
(assert (and (>= C19_12 0) (<= C19_12 1)))
(declare-const C19_13 Int)
(assert (and (>= C19_13 0) (<= C19_13 1)))
(declare-const C19_14 Int)
(assert (and (>= C19_14 0) (<= C19_14 1)))
(declare-const C19_15 Int)
(assert (and (>= C19_15 0) (<= C19_15 1)))
(declare-const N20 Int)
(assert (and (>= N20 0) (<= N20 1)))
(declare-const C20_0 Int)
(assert (and (>= C20_0 0) (<= C20_0 1)))
(declare-const C20_1 Int)
(assert (and (>= C20_1 0) (<= C20_1 1)))
(declare-const C20_2 Int)
(assert (and (>= C20_2 0) (<= C20_2 1)))
(declare-const C20_3 Int)
(assert (and (>= C20_3 0) (<= C20_3 1)))
(declare-const C20_4 Int)
(assert (and (>= C20_4 0) (<= C20_4 1)))
(declare-const C20_5 Int)
(assert (and (>= C20_5 0) (<= C20_5 1)))
(declare-const C20_6 Int)
(assert (and (>= C20_6 0) (<= C20_6 1)))
(declare-const C20_7 Int)
(assert (and (>= C20_7 0) (<= C20_7 1)))
(declare-const C20_8 Int)
(assert (and (>= C20_8 0) (<= C20_8 1)))
(declare-const C20_9 Int)
(assert (and (>= C20_9 0) (<= C20_9 1)))
(declare-const C20_10 Int)
(assert (and (>= C20_10 0) (<= C20_10 1)))
(declare-const C20_11 Int)
(assert (and (>= C20_11 0) (<= C20_11 1)))
(declare-const C20_12 Int)
(assert (and (>= C20_12 0) (<= C20_12 1)))
(declare-const C20_13 Int)
(assert (and (>= C20_13 0) (<= C20_13 1)))
(declare-const C20_14 Int)
(assert (and (>= C20_14 0) (<= C20_14 1)))
(declare-const C20_15 Int)
(assert (and (>= C20_15 0) (<= C20_15 1)))
(declare-const N21 Int)
(assert (and (>= N21 0) (<= N21 1)))
(declare-const C21_0 Int)
(assert (and (>= C21_0 0) (<= C21_0 1)))
(declare-const C21_1 Int)
(assert (and (>= C21_1 0) (<= C21_1 1)))
(declare-const C21_2 Int)
(assert (and (>= C21_2 0) (<= C21_2 1)))
(declare-const C21_3 Int)
(assert (and (>= C21_3 0) (<= C21_3 1)))
(declare-const C21_4 Int)
(assert (and (>= C21_4 0) (<= C21_4 1)))
(declare-const C21_5 Int)
(assert (and (>= C21_5 0) (<= C21_5 1)))
(declare-const C21_6 Int)
(assert (and (>= C21_6 0) (<= C21_6 1)))
(declare-const C21_7 Int)
(assert (and (>= C21_7 0) (<= C21_7 1)))
(declare-const C21_8 Int)
(assert (and (>= C21_8 0) (<= C21_8 1)))
(declare-const C21_9 Int)
(assert (and (>= C21_9 0) (<= C21_9 1)))
(declare-const C21_10 Int)
(assert (and (>= C21_10 0) (<= C21_10 1)))
(declare-const C21_11 Int)
(assert (and (>= C21_11 0) (<= C21_11 1)))
(declare-const C21_12 Int)
(assert (and (>= C21_12 0) (<= C21_12 1)))
(declare-const C21_13 Int)
(assert (and (>= C21_13 0) (<= C21_13 1)))
(declare-const C21_14 Int)
(assert (and (>= C21_14 0) (<= C21_14 1)))
(declare-const C21_15 Int)
(assert (and (>= C21_15 0) (<= C21_15 1)))
(declare-const N22 Int)
(assert (and (>= N22 0) (<= N22 1)))
(declare-const C22_0 Int)
(assert (and (>= C22_0 0) (<= C22_0 1)))
(declare-const C22_1 Int)
(assert (and (>= C22_1 0) (<= C22_1 1)))
(declare-const C22_2 Int)
(assert (and (>= C22_2 0) (<= C22_2 1)))
(declare-const C22_3 Int)
(assert (and (>= C22_3 0) (<= C22_3 1)))
(declare-const C22_4 Int)
(assert (= C22_4 0))
(declare-const C22_5 Int)
(assert (and (>= C22_5 0) (<= C22_5 1)))
(declare-const C22_6 Int)
(assert (and (>= C22_6 0) (<= C22_6 1)))
(declare-const C22_7 Int)
(assert (and (>= C22_7 0) (<= C22_7 1)))
(declare-const C22_8 Int)
(assert (and (>= C22_8 0) (<= C22_8 1)))
(declare-const C22_9 Int)
(assert (and (>= C22_9 0) (<= C22_9 1)))
(declare-const C22_10 Int)
(assert (and (>= C22_10 0) (<= C22_10 1)))
(declare-const C22_11 Int)
(assert (and (>= C22_11 0) (<= C22_11 1)))
(declare-const C22_12 Int)
(assert (and (>= C22_12 0) (<= C22_12 1)))
(declare-const C22_13 Int)
(assert (and (>= C22_13 0) (<= C22_13 1)))
(declare-const C22_14 Int)
(assert (and (>= C22_14 0) (<= C22_14 1)))
(declare-const C22_15 Int)
(assert (and (>= C22_15 0) (<= C22_15 1)))
(declare-const N24 Int)
(assert (and (>= N24 0) (<= N24 1)))
(declare-const C24_0 Int)
(assert (and (>= C24_0 0) (<= C24_0 1)))
(declare-const C24_1 Int)
(assert (and (>= C24_1 0) (<= C24_1 1)))
(declare-const C24_2 Int)
(assert (and (>= C24_2 0) (<= C24_2 1)))
(declare-const C24_3 Int)
(assert (and (>= C24_3 0) (<= C24_3 1)))
(declare-const C24_4 Int)
(assert (and (>= C24_4 0) (<= C24_4 1)))
(declare-const C24_5 Int)
(assert (and (>= C24_5 0) (<= C24_5 1)))
(declare-const C24_6 Int)
(assert (and (>= C24_6 0) (<= C24_6 1)))
(declare-const C24_7 Int)
(assert (and (>= C24_7 0) (<= C24_7 1)))
(declare-const C24_8 Int)
(assert (and (>= C24_8 0) (<= C24_8 1)))
(declare-const C24_9 Int)
(assert (and (>= C24_9 0) (<= C24_9 1)))
(declare-const C24_10 Int)
(assert (= C24_10 0))
(declare-const C24_11 Int)
(assert (and (>= C24_11 0) (<= C24_11 1)))
(declare-const C24_12 Int)
(assert (and (>= C24_12 0) (<= C24_12 1)))
(declare-const C24_13 Int)
(assert (and (>= C24_13 0) (<= C24_13 1)))
(declare-const C24_14 Int)
(assert (and (>= C24_14 0) (<= C24_14 1)))
(declare-const C24_15 Int)
(assert (and (>= C24_15 0) (<= C24_15 1)))
(declare-const N25 Int)
(assert (and (>= N25 0) (<= N25 1)))
(declare-const C25_0 Int)
(assert (and (>= C25_0 0) (<= C25_0 1)))
(declare-const C25_1 Int)
(assert (and (>= C25_1 0) (<= C25_1 1)))
(declare-const C25_2 Int)
(assert (and (>= C25_2 0) (<= C25_2 1)))
(declare-const C25_3 Int)
(assert (and (>= C25_3 0) (<= C25_3 1)))
(declare-const C25_4 Int)
(assert (and (>= C25_4 0) (<= C25_4 1)))
(declare-const C25_5 Int)
(assert (and (>= C25_5 0) (<= C25_5 1)))
(declare-const C25_6 Int)
(assert (and (>= C25_6 0) (<= C25_6 1)))
(declare-const C25_7 Int)
(assert (and (>= C25_7 0) (<= C25_7 1)))
(declare-const C25_8 Int)
(assert (and (>= C25_8 0) (<= C25_8 1)))
(declare-const C25_9 Int)
(assert (= C25_9 0))
(declare-const C25_10 Int)
(assert (and (>= C25_10 0) (<= C25_10 1)))
(declare-const C25_11 Int)
(assert (and (>= C25_11 0) (<= C25_11 1)))
(declare-const C25_12 Int)
(assert (and (>= C25_12 0) (<= C25_12 1)))
(declare-const C25_13 Int)
(assert (and (>= C25_13 0) (<= C25_13 1)))
(declare-const C25_14 Int)
(assert (and (>= C25_14 0) (<= C25_14 1)))
(declare-const C25_15 Int)
(assert (and (>= C25_15 0) (<= C25_15 1)))
(declare-const N28 Int)
(assert (and (>= N28 0) (<= N28 1)))
(declare-const C28_0 Int)
(assert (and (>= C28_0 0) (<= C28_0 1)))
(declare-const C28_1 Int)
(assert (and (>= C28_1 0) (<= C28_1 1)))
(declare-const C28_2 Int)
(assert (and (>= C28_2 0) (<= C28_2 1)))
(declare-const C28_3 Int)
(assert (and (>= C28_3 0) (<= C28_3 1)))
(declare-const C28_4 Int)
(assert (and (>= C28_4 0) (<= C28_4 1)))
(declare-const C28_5 Int)
(assert (and (>= C28_5 0) (<= C28_5 1)))
(declare-const C28_6 Int)
(assert (and (>= C28_6 0) (<= C28_6 1)))
(declare-const C28_7 Int)
(assert (and (>= C28_7 0) (<= C28_7 1)))
(declare-const C28_8 Int)
(assert (and (>= C28_8 0) (<= C28_8 1)))
(declare-const C28_9 Int)
(assert (and (>= C28_9 0) (<= C28_9 1)))
(declare-const C28_10 Int)
(assert (and (>= C28_10 0) (<= C28_10 1)))
(declare-const C28_11 Int)
(assert (and (>= C28_11 0) (<= C28_11 1)))
(declare-const C28_12 Int)
(assert (and (>= C28_12 0) (<= C28_12 1)))
(declare-const C28_13 Int)
(assert (and (>= C28_13 0) (<= C28_13 1)))
(declare-const C28_14 Int)
(assert (and (>= C28_14 0) (<= C28_14 1)))
(declare-const C28_15 Int)
(assert (and (>= C28_15 0) (<= C28_15 1)))
(declare-const I0 Int)
(assert (and (>= I0 0) (<= I0 1)))
(assert (<= N25 (- 1 I0)))
(assert (<= I0 N1))
(declare-const I1 Int)
(assert (and (>= I1 0) (<= I1 1)))
(assert (<= N10 (- 1 I1)))
(assert (<= I1 N17))
(declare-const I2 Int)
(assert (and (>= I2 0) (<= I2 1)))
(assert (<= N28 (- 1 I2)))
(assert (<= I2 N22))
(declare-const I3 Int)
(assert (and (>= I3 0) (<= I3 1)))
(assert (<= N2 (- 1 I3)))
(assert (<= I3 N12))
(declare-const I4 Int)
(assert (and (>= I4 0) (<= I4 1)))
(assert (<= N22 (- 1 I4)))
(assert (<= I4 N12))
(declare-const I5 Int)
(assert (and (>= I5 0) (<= I5 1)))
(assert (<= N2 (- 1 I5)))
(assert (<= I5 N12))
(declare-const I6 Int)
(assert (and (>= I6 0) (<= I6 1)))
(assert (<= N2 (- 1 I6)))
(assert (<= I6 N12))
(declare-const I7 Int)
(assert (and (>= I7 0) (<= I7 1)))
(assert (<= N11 (- 1 I7)))
(assert (<= I7 N12))
(declare-const I8 Int)
(assert (and (>= I8 0) (<= I8 1)))
(assert (<= N2 (- 1 I8)))
(assert (<= I8 N12))
(declare-const I9 Int)
(assert (and (>= I9 0) (<= I9 1)))
(assert (<= N11 (- 1 I9)))
(assert (<= I9 N12))
(declare-const I10 Int)
(assert (and (>= I10 0) (<= I10 1)))
(assert (<= N22 (- 1 I10)))
(assert (<= I10 N12))
(declare-const I11 Int)
(assert (and (>= I11 0) (<= I11 1)))
(assert (<= N13 (- 1 I11)))
(assert (<= I11 N12))
(declare-const I12 Int)
(assert (and (>= I12 0) (<= I12 1)))
(assert (<= N24 (- 1 I12)))
(assert (<= I12 N12))
(declare-const I13 Int)
(assert (and (>= I13 0) (<= I13 1)))
(assert (<= N24 (- 1 I13)))
(assert (<= I13 N12))
(declare-const I14 Int)
(assert (and (>= I14 0) (<= I14 1)))
(assert (<= N24 (- 1 I14)))
(assert (<= I14 N12))
(declare-const I15 Int)
(assert (and (>= I15 0) (<= I15 1)))
(assert (<= N17 (- 1 I15)))
(assert (<= I15 N12))
(declare-const I16 Int)
(assert (and (>= I16 0) (<= I16 1)))
(assert (<= N11 (- 1 I16)))
(assert (<= I16 N12))
(declare-const I17 Int)
(assert (and (>= I17 0) (<= I17 1)))
(assert (<= N2 (- 1 I17)))
(assert (<= I17 N12))
(declare-const I18 Int)
(assert (and (>= I18 0) (<= I18 1)))
(assert (<= N18 (- 1 I18)))
(assert (<= I18 N12))
(declare-const I19 Int)
(assert (and (>= I19 0) (<= I19 1)))
(assert (<= N2 (- 1 I19)))
(assert (<= I19 N12))
(declare-const I20 Int)
(assert (and (>= I20 0) (<= I20 1)))
(assert (<= N24 (- 1 I20)))
(assert (<= I20 N12))
(declare-const I21 Int)
(assert (and (>= I21 0) (<= I21 1)))
(assert (<= N22 (- 1 I21)))
(assert (<= I21 N12))
(declare-const I22 Int)
(assert (and (>= I22 0) (<= I22 1)))
(assert (<= N11 (- 1 I22)))
(assert (<= I22 N12))
(declare-const I23 Int)
(assert (and (>= I23 0) (<= I23 1)))
(assert (<= N2 (- 1 I23)))
(assert (<= I23 N12))
(declare-const I24 Int)
(assert (and (>= I24 0) (<= I24 1)))
(assert (<= N2 (- 1 I24)))
(assert (<= I24 N12))
(declare-const I25 Int)
(assert (and (>= I25 0) (<= I25 1)))
(assert (<= N2 (- 1 I25)))
(assert (<= I25 N12))
(declare-const I26 Int)
(assert (and (>= I26 0) (<= I26 1)))
(assert (<= N18 (- 1 I26)))
(assert (<= I26 N12))
(declare-const I27 Int)
(assert (and (>= I27 0) (<= I27 1)))
(assert (<= N19 (- 1 I27)))
(assert (<= I27 N12))
(declare-const I28 Int)
(assert (and (>= I28 0) (<= I28 1)))
(assert (<= N19 (- 1 I28)))
(assert (<= I28 N12))
(declare-const I29 Int)
(assert (and (>= I29 0) (<= I29 1)))
(assert (<= N13 (- 1 I29)))
(assert (<= I29 N12))
(declare-const I30 Int)
(assert (and (>= I30 0) (<= I30 1)))
(assert (<= N24 (- 1 I30)))
(assert (<= I30 N12))
(declare-const I31 Int)
(assert (and (>= I31 0) (<= I31 1)))
(assert (<= N22 (- 1 I31)))
(assert (<= I31 N12))
(declare-const I32 Int)
(assert (and (>= I32 0) (<= I32 1)))
(assert (<= N11 (- 1 I32)))
(assert (<= I32 N12))
(declare-const I33 Int)
(assert (and (>= I33 0) (<= I33 1)))
(assert (<= N11 (- 1 I33)))
(assert (<= I33 N12))
(declare-const I34 Int)
(assert (and (>= I34 0) (<= I34 1)))
(assert (<= N24 (- 1 I34)))
(assert (<= I34 N12))
(declare-const I35 Int)
(assert (and (>= I35 0) (<= I35 1)))
(assert (<= N24 (- 1 I35)))
(assert (<= I35 N12))
(declare-const I36 Int)
(assert (and (>= I36 0) (<= I36 1)))
(assert (<= N17 (- 1 I36)))
(assert (<= I36 N12))
(declare-const I37 Int)
(assert (and (>= I37 0) (<= I37 1)))
(assert (<= N2 (- 1 I37)))
(assert (<= I37 N12))
(declare-const I38 Int)
(assert (and (>= I38 0) (<= I38 1)))
(assert (<= N22 (- 1 I38)))
(assert (<= I38 N12))
(declare-const I39 Int)
(assert (and (>= I39 0) (<= I39 1)))
(assert (<= N2 (- 1 I39)))
(assert (<= I39 N12))
(declare-const I40 Int)
(assert (and (>= I40 0) (<= I40 1)))
(assert (<= N11 (- 1 I40)))
(assert (<= I40 N12))
(declare-const I41 Int)
(assert (and (>= I41 0) (<= I41 1)))
(assert (<= N2 (- 1 I41)))
(assert (<= I41 N12))
(declare-const I42 Int)
(assert (and (>= I42 0) (<= I42 1)))
(assert (<= N2 (- 1 I42)))
(assert (<= I42 N12))
(declare-const I43 Int)
(assert (and (>= I43 0) (<= I43 1)))
(assert (<= N21 (- 1 I43)))
(assert (<= I43 N12))
(declare-const I44 Int)
(assert (and (>= I44 0) (<= I44 1)))
(assert (<= N11 (- 1 I44)))
(assert (<= I44 N12))
(declare-const I45 Int)
(assert (and (>= I45 0) (<= I45 1)))
(assert (<= N22 (- 1 I45)))
(assert (<= I45 N12))
(declare-const I46 Int)
(assert (and (>= I46 0) (<= I46 1)))
(assert (<= N20 (- 1 I46)))
(assert (<= I46 N12))
(declare-const I47 Int)
(assert (and (>= I47 0) (<= I47 1)))
(assert (<= N17 (- 1 I47)))
(assert (<= I47 N12))
(assert (= I0 N1))
(assert (= I3 N12))
(assert (= I4 N12))
(assert (= I5 N12))
(assert (= I1 N17))
(assert (>= 16 (+ N1 N2 N10 N11 N12 N13 N17 N18 N19 N20 N21 N22 N24 N25 N28)))
(assert (= N1 (+ C1_0 C1_1 C1_2 C1_3 C1_4 C1_5 C1_6 C1_7 C1_8 C1_9 C1_10 C1_11 C1_12 C1_13 C1_14 C1_15)))
(assert (= N2 (+ C2_0 C2_1 C2_2 C2_3 C2_4 C2_5 C2_6 C2_7 C2_8 C2_9 C2_10 C2_11 C2_12 C2_13 C2_14 C2_15)))
(assert (= N10 (+ C10_0 C10_1 C10_2 C10_3 C10_4 C10_5 C10_6 C10_7 C10_8 C10_9 C10_10 C10_11 C10_12 C10_13 C10_14 C10_15)))
(assert (= N11 (+ C11_0 C11_1 C11_2 C11_3 C11_4 C11_5 C11_6 C11_7 C11_8 C11_9 C11_10 C11_11 C11_12 C11_13 C11_14 C11_15)))
(assert (= N12 (+ C12_0 C12_1 C12_2 C12_3 C12_4 C12_5 C12_6 C12_7 C12_8 C12_9 C12_10 C12_11 C12_12 C12_13 C12_14 C12_15)))
(assert (= N13 (+ C13_0 C13_1 C13_2 C13_3 C13_4 C13_5 C13_6 C13_7 C13_8 C13_9 C13_10 C13_11 C13_12 C13_13 C13_14 C13_15)))
(assert (= N17 (+ C17_0 C17_1 C17_2 C17_3 C17_4 C17_5 C17_6 C17_7 C17_8 C17_9 C17_10 C17_11 C17_12 C17_13 C17_14 C17_15)))
(assert (= N18 (+ C18_0 C18_1 C18_2 C18_3 C18_4 C18_5 C18_6 C18_7 C18_8 C18_9 C18_10 C18_11 C18_12 C18_13 C18_14 C18_15)))
(assert (= N19 (+ C19_0 C19_1 C19_2 C19_3 C19_4 C19_5 C19_6 C19_7 C19_8 C19_9 C19_10 C19_11 C19_12 C19_13 C19_14 C19_15)))
(assert (= N20 (+ C20_0 C20_1 C20_2 C20_3 C20_4 C20_5 C20_6 C20_7 C20_8 C20_9 C20_10 C20_11 C20_12 C20_13 C20_14 C20_15)))
(assert (= N21 (+ C21_0 C21_1 C21_2 C21_3 C21_4 C21_5 C21_6 C21_7 C21_8 C21_9 C21_10 C21_11 C21_12 C21_13 C21_14 C21_15)))
(assert (= N22 (+ C22_0 C22_1 C22_2 C22_3 C22_4 C22_5 C22_6 C22_7 C22_8 C22_9 C22_10 C22_11 C22_12 C22_13 C22_14 C22_15)))
(assert (= N24 (+ C24_0 C24_1 C24_2 C24_3 C24_4 C24_5 C24_6 C24_7 C24_8 C24_9 C24_10 C24_11 C24_12 C24_13 C24_14 C24_15)))
(assert (= N25 (+ C25_0 C25_1 C25_2 C25_3 C25_4 C25_5 C25_6 C25_7 C25_8 C25_9 C25_10 C25_11 C25_12 C25_13 C25_14 C25_15)))
(assert (= N28 (+ C28_0 C28_1 C28_2 C28_3 C28_4 C28_5 C28_6 C28_7 C28_8 C28_9 C28_10 C28_11 C28_12 C28_13 C28_14 C28_15)))
(assert (>= 1 (+ C1_0 C2_0 C10_0 C11_0 C12_0 C13_0 C17_0 C18_0 C19_0 C20_0 C21_0 C22_0 C24_0 C25_0 C28_0)))
(assert (>= 1 (+ C1_1 C2_1 C10_1 C11_1 C12_1 C13_1 C17_1 C18_1 C19_1 C20_1 C21_1 C22_1 C24_1 C25_1 C28_1)))
(assert (>= 1 (+ C1_2 C2_2 C10_2 C11_2 C12_2 C13_2 C17_2 C18_2 C19_2 C20_2 C21_2 C22_2 C24_2 C25_2 C28_2)))
(assert (>= 1 (+ C1_3 C2_3 C10_3 C11_3 C12_3 C13_3 C17_3 C18_3 C19_3 C20_3 C21_3 C22_3 C24_3 C25_3 C28_3)))
(assert (>= 1 (+ C1_4 C2_4 C10_4 C11_4 C12_4 C13_4 C17_4 C18_4 C19_4 C20_4 C21_4 C22_4 C24_4 C25_4 C28_4)))
(assert (>= 1 (+ C1_5 C2_5 C10_5 C11_5 C12_5 C13_5 C17_5 C18_5 C19_5 C20_5 C21_5 C22_5 C24_5 C25_5 C28_5)))
(assert (>= 1 (+ C1_6 C2_6 C10_6 C11_6 C12_6 C13_6 C17_6 C18_6 C19_6 C20_6 C21_6 C22_6 C24_6 C25_6 C28_6)))
(assert (>= 1 (+ C1_7 C2_7 C10_7 C11_7 C12_7 C13_7 C17_7 C18_7 C19_7 C20_7 C21_7 C22_7 C24_7 C25_7 C28_7)))
(assert (>= 1 (+ C1_8 C2_8 C10_8 C11_8 C12_8 C13_8 C17_8 C18_8 C19_8 C20_8 C21_8 C22_8 C24_8 C25_8 C28_8)))
(assert (>= 1 (+ C1_9 C2_9 C10_9 C11_9 C12_9 C13_9 C17_9 C18_9 C19_9 C20_9 C21_9 C22_9 C24_9 C25_9 C28_9)))
(assert (>= 1 (+ C1_10 C2_10 C10_10 C11_10 C12_10 C13_10 C17_10 C18_10 C19_10 C20_10 C21_10 C22_10 C24_10 C25_10 C28_10)))
(assert (>= 1 (+ C1_11 C2_11 C10_11 C11_11 C12_11 C13_11 C17_11 C18_11 C19_11 C20_11 C21_11 C22_11 C24_11 C25_11 C28_11)))
(assert (>= 1 (+ C1_12 C2_12 C10_12 C11_12 C12_12 C13_12 C17_12 C18_12 C19_12 C20_12 C21_12 C22_12 C24_12 C25_12 C28_12)))
(assert (>= 1 (+ C1_13 C2_13 C10_13 C11_13 C12_13 C13_13 C17_13 C18_13 C19_13 C20_13 C21_13 C22_13 C24_13 C25_13 C28_13)))
(assert (>= 1 (+ C1_14 C2_14 C10_14 C11_14 C12_14 C13_14 C17_14 C18_14 C19_14 C20_14 C21_14 C22_14 C24_14 C25_14 C28_14)))
(assert (>= 1 (+ C1_15 C2_15 C10_15 C11_15 C12_15 C13_15 C17_15 C18_15 C19_15 C20_15 C21_15 C22_15 C24_15 C25_15 C28_15)))
(assert (= N2 0))
(assert (= N10 0))
(assert (= N11 0))
(assert (>= 1 (+ I6 I7 I8 I9 I10 I11 I12 I13 I14 I15 I16 I17 I18 I19 I20 I21 I22 I23 I24 I25 I26 I27 I28 I29 I30 I31 I32 I33 I34 I35 I36 I37 I38 I39 I40 I41 I42 I43 I44 I45 I46 I47 0)))
(assert (>= 4 (+ I3 I4 I5 I6 I7 I8 I9 I10 I11 I12 I13 I14 I15 I16 I17 I18 I19 I20 I21 I22 I23 I24 I25 I26 I27 I28 I29 I30 I31 I32 I33 I34 I35 I36 I37 I38 I39 I40 I41 I42 I43 I44 I45 I46 I47 0)))
(assert (= N13 0))
(assert (= N18 0))
(assert (= N19 0))
(assert (= N20 0))
(assert (= N21 0))
(assert (>= 1 (+ I2 0)))
(assert (>= 4 (+ I2 0)))
(assert (= N24 0))
(assert (= N25 0))
(assert (= N28 0))
(define-fun W47 () Int
   4
)
(define-fun W46 () Int
   8
)
(define-fun W45 () Int
   16
)
(define-fun W44 () Int
   32
)
(define-fun W43 () Int
   64
)
(define-fun W42 () Int
   128
)
(define-fun W41 () Int
   256
)
(define-fun W40 () Int
   512
)
(define-fun W39 () Int
   1024
)
(define-fun W38 () Int
   2048
)
(define-fun W37 () Int
   4096
)
(define-fun W36 () Int
   8192
)
(define-fun W35 () Int
   16384
)
(define-fun W34 () Int
   32768
)
(define-fun W33 () Int
   65536
)
(define-fun W32 () Int
   131072
)
(define-fun W31 () Int
   262144
)
(define-fun W30 () Int
   524288
)
(define-fun W29 () Int
   1048576
)
(define-fun W28 () Int
   2097152
)
(define-fun W27 () Int
   4194304
)
(define-fun W26 () Int
   8388608
)
(define-fun W25 () Int
   16777216
)
(define-fun W24 () Int
   33554432
)
(define-fun W23 () Int
   67108864
)
(define-fun W22 () Int
   134217728
)
(define-fun W21 () Int
   268435456
)
(define-fun W20 () Int
   536870912
)
(define-fun W19 () Int
   1073741824
)
(define-fun W18 () Int
   2147483648
)
(define-fun W17 () Int
   4294967296
)
(define-fun W16 () Int
   8589934592
)
(define-fun W15 () Int
   17179869184
)
(define-fun W14 () Int
   34359738368
)
(define-fun W13 () Int
   68719476736
)
(define-fun W12 () Int
   137438953472
)
(define-fun W11 () Int
   274877906944
)
(define-fun W10 () Int
   549755813888
)
(define-fun W9 () Int
   1099511627776
)
(define-fun W8 () Int
   2199023255552
)
(define-fun W7 () Int
   4398046511104
)
(define-fun W6 () Int
   8796093022208
)
(define-fun W5 () Int
   17592186044416
)
(define-fun W4 () Int
   35184372088832
)
(define-fun W3 () Int
   70368744177664
)
(define-fun W2 () Int
   140737488355328
)
(define-fun W1 () Int
   281474976710656
)
(define-fun W0 () Int
   562949953421312
)
;(assert (= I0 1))
;(assert (= I1 1))
(assert (>= 50 (+ I0 I1 I2 I3 I4 I5 I6 I7 I8 I9 I10 I11 I12 I13 I14 I15 I16 I17 I18 I19 I20 I21 I22 I23 I24 I25 I26 I27 I28 I29 I30 I31 I32 I33 I34 I35 I36 I37 I38 I39 I40 I41 I42 I43 I44 I45 I46 I47 0)))
(maximize (+ 0 (* I0 W0) (* I1 W1) (* I2 W2) (* I3 W3) (* I4 W4) (* I5 W5) (* I6 W6) (* I7 W7) (* I8 W8) (* I9 W9) (* I10 W10) (* I11 W11) (* I12 W12) (* I13 W13) (* I14 W14) (* I15 W15) (* I16 W16) (* I17 W17) (* I18 W18) (* I19 W19) (* I20 W20) (* I21 W21) (* I22 W22) (* I23 W23) (* I24 W24) (* I25 W25) (* I26 W26) (* I27 W27) (* I28 W28) (* I29 W29) (* I30 W30) (* I31 W31) (* I32 W32) (* I33 W33) (* I34 W34) (* I35 W35) (* I36 W36) (* I37 W37) (* I38 W38) (* I39 W39) (* I40 W40) (* I41 W41) (* I42 W42) (* I43 W43) (* I44 W44) (* I45 W45) (* I46 W46) (* I47 W47)))
(check-sat)
(eval I0)
(eval I1)
;(get-objectives)